1. $T$ : Type
\\[0ex]2. $R$ : $T$$\rightarrow$$T$$\rightarrow\mathbb{P}$
\\[0ex]3. Refl($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]4. Trans($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\vdash$  Refl($T$;$a$,$b$.$R$($a$,$b$) \& $R$($b$,$a$))